%%%%%%%%%%%%%%%%%%%%
%%% BEGIN MACROS %%%
%%%%%%%%%%%%%%%%%%%%

% ENVIRONMENTS
\iffalse
\newtheorem{definition}{Definizione}
\newtheorem{notation}{Notazione}
\newtheorem{proposition}{Proposizione}
\newtheorem{theorem}{Teorema}
\newtheorem{example}{Esempio}

\newenvironment{proof}{
\noindent\emph{Dimostrazione.}
}{
\hfill$\Box$
}
\else
\theoremstyle{plain}
\newtheorem{theorem}{Teorema}
\newtheorem{proposition}{Proposizione}

\theoremstyle{definition}
\newtheorem{defn}{Definizione}

\newtheorem{example}{Esempio}

\theoremstyle{remark}
\newtheorem{notation}{Notazione}

\newenvironment{definition}[1][1]{
\begin{defn}[#1]
\renewcommand{\qedhere}{$\blacksquare$}
}{
\hfill\qedhere
\end{defn}
}
\fi

\newcommand{\rnf}{\mathsf{rnf}}
\newcommand{\nf}{\mathsf{nf}}

% ACCEPTANCE SETS
\newcommand{\amin}[1]{\mathit{min}~#1}
\newcommand{\asat}[1]{\mathit{sat}~#1}
\newcommand{\acar}[1]{\mathit{car}~#1}

% CONTRACT SYNTAX
\newcommand{\nullc}{\mathbf{0}}
\newcommand{\winc}{\mathbf{1}}
\newcommand{\recc}{\mathsf{rec}~}
\newcommand{\contract}[2]{#1:#2}

\newcommand{\automaton}[1]{(Q_{#1}, \Sigma_{#1}, \delta_{#1}, p_{#1}, F_{#1})}
\newcommand{\tauclosure}{\text{$\tau$-$\mathsf{closure}$}}
\newcommand{\stable}{\mathsf{stable}}

% PROCESS SYNTAX
\newcommand{\nullp}{\mathbf{0}}
\newcommand{\parop}{\mathbin{\|}}
\newcommand{\session}[2]{#1^{#2}}
\newcommand{\sclient}{\circ}
\newcommand{\sservice}{\bullet}
\newcommand{\emptycontext}{\tau}

% PROCESS FUNCTIONS
\newcommand{\nm}{\mathsf{names}}
\newcommand{\fn}{\mathsf{fn}}
\newcommand{\bn}{\mathsf{bn}}
\newcommand{\dom}{\mathsf{dom}}
\newcommand{\subst}[2]{\{#1/#2\}}
\newcommand{\loc}{\mathsf{loc}}

% TRANSITION RELATIONS
\newcommand{\acc}[1]{\stackrel{#1}{\longmapsto}}
\newcommand{\nacc}[1]{\longarrownot\acc{#1}}
\newcommand{\wacc}[1]{\stackrel{#1}{\Longmapsto}}
\newcommand{\nwacc}[1]{\Longarrownot\wacc{#1}}
\newcommand{\lred}[1]{\stackrel{#1}{\longrightarrow}}
\newcommand{\xlred}[1]{\xrightarrow{\,#1\,}}
\newcommand{\lmap}[1]{\stackrel{#1}{\longmapsto}}
\newcommand{\xlmap}[1]{\xmapsto{\,#1\,}}
\newcommand{\nlmap}[1]{\longarrownot\lmap{#1}}
\newcommand{\wlred}[1]{\stackrel{#1}{\Longrightarrow}}
\newcommand{\nwlred}[1]{\Longarrownot\wlred{#1}}
\newcommand{\nlred}[1]{\longarrownot\lred{#1}}

% DEDUCTION SYSTEMS
\newcommand{\rulename}[1]{{\textsc{(#1)}}}

\newcommand{\mathaxiom}[1]{
  \begin{array}{@{}c@{}}
    \textstyle#1
  \end{array}
}

\newcommand{\mathrule}[2]{
  \begin{array}{@{}c@{}}
    \textstyle#1 \\
    \hline
    \textstyle#2
  \end{array}
}

\newcommand{\nmathaxiom}[2]{
  \mathaxiom{%
    {\scriptsize\rulename{#1}}\hfill\\%
    #2%
  }
}

\newcommand{\nmathrule}[3]{
  \mathrule{%
    {\scriptsize\rulename{#1}}\hfill\\%
    #2%
  }{%
    #3%
  }
}

% FUNCTIONS OVER CONTRACTS
\newcommand{\initc}{\mathsf{init}}
\newcommand{\namesc}{\mathsf{names}}
\newcommand{\co}[1]{\overline{#1}}
\newcommand{\coset}[1]{\overline{#1}}

% CONDITIONS
\newcommand{\bsem}[1]{\llbracket#1\rrbracket}
\newcommand{\btrue}{\mathsf{tt}}
\newcommand{\bfalse}{\mathsf{ff}}

% RELATIONS OVER CONTRACTS
\newcommand{\rset}[1]{\textsc{#1}}
\newcommand{\diverge}{\mathclose{\uparrow}}
\newcommand{\converge}{\mathclose{\downarrow}}

% RELATIONS
\newcommand{\eqdef}{\stackrel{\text{def}}{=}}
\newcommand{\iffdef}{\stackrel{\text{def}}{\iff}}
\newcommand{\subc}{\preceq}
\newcommand{\eqc}{\simeq}
\newcommand{\subt}{\mathrel{<:}}
\newcommand{\scomp}{\dashv}
\newcommand{\rel}[1]{\mathrel{\mathcal{#1}}}
\newcommand{\tort}{\mathrel{\emptyt}}
\newcommand{\allowedby}{:}

%%%%%%%%%%%%%%%%%%
%%% END MACROS %%%
%%%%%%%%%%%%%%%%%%

